Lurch Deductive Engine: Tutorial: Methods in each LC subclass

This tutorial assumes you know how to construct LC instances; if not, see the tutorial on Constructing LCs. This tutorial covers the most common methods available in each of the common LC subclasses, such as symbols, declarations, etc.

(Each piece of sample code below is written as if it were a script sitting in the root folder of this source code repository, and run from there with the command-line tools node. If you place your scripts in another folder, you will need to adjust the path in each import statement accordingly. If you have not yet set up a copy of this repository with the appropriate Node.js version installed, see our GitHub README, which explains how to do so.)

Symbols have text and sometimes a value

Every Symbol instance gives access to the text of the symbol itself, using the .text() method. If the Symbol you've created can be interpreted as an integer, a real number (floating point), or a string, you can specify this with an attribute, as shown below, and then the .value() method will respect that attribute and convert the Symbol into a JavaScript atomic value.

import { LurchSymbol } from './src/index.js'

const x = new LurchSymbol( 'x' )
console.log( 'Text of x:', x.text() )

const closeToPi = new LurchSymbol( '3.14159' )
console.log( 'Value of pi:', closeToPi.value() ) // does not work
closeToPi.setAttribute( 'evaluate as', 'real' )
console.log( 'Value of pi:', closeToPi.value() ) // now it works

// Console output:
Text of x: x
Value of pi: undefined
Value of pi: 3.14159

Applications have an operator and operands

The "head" (or first child) of an Application expression is the operator and all the remaining children are the operands. This is because we use prefix notation in putdown and throughout the LDE, in the style of LISP and related languages.

import { LogicConcept } from './src/index.js'

const expr1 = LogicConcept.fromPutdown( '(- (* 2 (^ x 2)) 1)' )[0]
console.log( 'Outermost operator:', expr1.operator().toPutdown() )
console.log( 'Its operands:', expr1.operands().map( x => x.toPutdown() ) )
const expr2 = expr1.child( 1 )
console.log( 'Next operator:', expr2.operator().toPutdown() )
console.log( 'Its operands:', expr2.operands().map( x => x.toPutdown() ) )
const expr3 = expr2.child( 2 )
console.log( 'Innermost operator:', expr3.operator().toPutdown() )
console.log( 'Its operands:', expr3.operands().map( x => x.toPutdown() ) )

// Console output:
Outermost operator: -
Its operands: [ '(* 2 (^ x 2))', '1' ]
Next operator: *
Its operands: [ '2', '(^ x 2)' ]
Innermost operator: ^
Its operands: [ 'x', '2' ]

For any expression at all, you can fetch its full list of children, which for an Application is the operator and operands in one list. You can also ask whether an expression is the outermost one in the tree in which it sits (meaning it's inside an Environment, or not inside any parent), and you can fetch the outermost expression surrounding an expression as well.

console.log( 'Children of outer expression:',
             expr1.children().map( x => x.toPutdown() ) )
console.log( 'That one is outermost?', expr1.isOutermost() )
console.log( 'Is one of its children outermost?', expr2.isOutermost() )
console.log( 'Fetch outermost from within:',
             expr2.getOutermost().toPutdown() )

// Console output:
Children of outer expression: [ '-', '(* 2 (^ x 2))', '1' ]
That one is outermost? true
Is one of its children outermost? false
Fetch outermost from within: (- (* 2 (^ x 2)) 1)

Bindings have a head, bound variables, and a body

This is very similar to the previous case, except for the components of a Binding expression rather than an Application expression. One difference is that you can fetch either the names of the bound variables, as shown below, or the actual bound variable objects (as Symbols) that sit inside the expression, using a different function.

const binding = LogicConcept.fromPutdown( '(forall x y z , (P x y z))' )[0]
console.log( 'Quantifier:', binding.head().toPutdown() )
console.log( 'Bound variables:', binding.boundVariableNames() )
console.log( 'Body:', binding.body().toPutdown() )

// Console output:
file:///Users/monks/Dropbox/files/monkware/git/lde/tutorial-tmp-file-Methods%20in%20each%20LC%20subclass.md.js:31
console.log( 'Quantifier:', binding.head().toPutdown() )
                                    ^

TypeError: binding.head is not a function
    at file:///Users/monks/Dropbox/files/monkware/git/lde/tutorial-tmp-file-Methods%20in%20each%20LC%20subclass.md.js:31:37
    at ModuleJob.run (node:internal/modules/esm/module_job:198:25)
    at async Promise.all (index 0)
    at async ESMLoader.import (node:internal/modules/esm/loader:409:24)
    at async loadESM (node:internal/process/esm_loader:85:5)
    at async handleMainPromise (node:internal/modules/run_main:61:12)

Node.js v18.4.0

And the list of children of a binding are the head, bound variables, and body, in the order they appear in the binding.

console.log( binding.children().map( x => x.toPutdown() ) )

Declarations have a type, symbols, and optionally a body

A Declaration can be of one of only two types: a constant declaration or a variable declaration. There are two static constants in the Declaration class for this purpose, Declaration.Constant and Declaration.Variable, as shown below. You can query the type(), list of symbols(), and body(), although not every declaration has a body.

import { Declaration } from './src/index.js'

const decl = LogicConcept.fromPutdown( '[a b c var (> (+ a b) c)]' )[0]
console.log( 'Declaration type:', decl.type() )
console.log( 'How to verify that it\'s a variable declaration:',
             decl.type() == Declaration.Variable )
console.log( 'Declared symbols:', decl.symbols().map( x => x.toPutdown() ) )
console.log( 'Declaration body:', decl.body().toPutdown() )

If there were no body, as in [a b c var], then decl.body() would return undefined.

Environments have conclusions

As with any LC, you can get the children of an environment with the usual children() method, but you can also ask for its set of conclusions(). (See that link for the definition of "conclusions" in an Environment.) You can also ask whether any LC is a conclusion in one of its ancestors.

const env = LogicConcept.fromPutdown( '{ A :{ B C } { :D E } }' )[0]
console.log( 'Children:', env.children().map( x => x.toPutdown() ) )
console.log( 'Conclusions:', env.conclusions().map( x => x.toPutdown() ) )
const D = env.child( 2 ).child( 0 )
console.log( 'D is a conclusion?', D.isAConclusionIn( env ) )